Termination w.r.t. Q proof of TRS/AG01#3.15.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

average(s(x), y) → average(x, s(y))
average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0
average(0, s(0)) → 0
average(0, s(s(0))) → s(0)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

average(s(x), y) → average(x, s(y))
average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0
average(0, s(0)) → 0
average(0, s(s(0))) → s(0)

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

average(s(x), y) → average(x, s(y))
average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0
average(0, s(0)) → 0
average(0, s(s(0))) → s(0)

The set Q consists of the following terms:

average(s(x0), x1)
average(x0, s(s(s(x1))))
average(0, 0)
average(0, s(0))
average(0, s(s(0)))

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

AVERAGE(x, s(s(s(y)))) → AVERAGE(s(x), y)
AVERAGE(s(x), y) → AVERAGE(x, s(y))

The TRS R consists of the following rules:

average(s(x), y) → average(x, s(y))
average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0
average(0, s(0)) → 0
average(0, s(s(0))) → s(0)

The set Q consists of the following terms:

average(s(x0), x1)
average(x0, s(s(s(x1))))
average(0, 0)
average(0, s(0))
average(0, s(s(0)))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

AVERAGE(x, s(s(s(y)))) → AVERAGE(s(x), y)
AVERAGE(s(x), y) → AVERAGE(x, s(y))

The TRS R consists of the following rules:

average(s(x), y) → average(x, s(y))
average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0
average(0, s(0)) → 0
average(0, s(s(0))) → s(0)

The set Q consists of the following terms:

average(s(x0), x1)
average(x0, s(s(s(x1))))
average(0, 0)
average(0, s(0))
average(0, s(s(0)))

We have to consider all minimal (P,Q,R)-chains.